interleaved\_family($T$;$I$;$L$;$L_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$f$:($i$:$I$$\rightarrow$\{0..$\parallel$$L$($i$)$\parallel^{-}$\}$\rightarrow$\{0..$\parallel$$L_{2}$$\parallel^{-}$\}). interleaved\_family\_occurence($T$;$I$;$L$;$L_{2}$;$f$)